We have a sub-language talking about individuals.

We call those that sub-language terms.

And we have another language in which we can make propositions.

You think about terms, they always denote individuals.

The father, the father, the father of her, the great grandfather,

is or was probably some guy somewhere an individual.

So this term, father of father of father of x, is an individual as well.

And then we have these propositions which are things that will eventually denote truth values,

things like the moon is made out of green cheese,

which is a statement which can be true or false.

By now we know it's false.

Which is really about the relation of two objects which are individuals,

namely the moon, an individual, and well, green cheese is maybe not an individual.

It's another property.

So it's a property of an individual of the moon.

But if we have Peter loves Mary, then we have a relation between two individuals.

Good.

Okay.

That's the formal language.

Relatively complex formal language.

Which is this complex because first-order logic is kind of a syntactically funny member of formal languages.

You have to kind of craft it this funny way so that it actually has the good properties.

If you go higher to so-called higher-order logics, you can write them down in this much, much easier.

Much more regular objects as languages go.

But they don't have the right properties.

So we have to do this kind of two-layered approach.

Because, and that's important,

in the central new innovation of first-order logic,

we are restricting ourselves to individual variables.

The thing we cannot write down in first-order logic is for all p, p of a or p of b.

Why is that?

Because we make terms from variables and functions and so on.

But we have no way of smuggling a variable in here.

Here, for the functions, we only allow a predefined number of constant functions.

And for the, where are they?

Here, we only allow predicates from the signatures, no variables.

You have no rule that would allow us to apply a variable to an argument or a bunch of arguments.

Okay?

So this is not in first-order logic.

Which is a great pity because we need it for math.

We want to write down the induction axiom for natural numbers.

And that is something where we want to write for all sets S such that

S of zero and for n, all n, S of n implies S of n plus one.

All of that implies for all x, S of x, that's the induction axiom.

We cannot write it down because we have a variable S applied as a predicate here.

We can't write it down.

And by the way, I told you the story about Kurt Gödel.

Whenever you can do this, you can build paradoxes.

You can write down the sentence.

This sentence cannot be proved in that calculus.